/*
 * Define the contracts associated with sequences and collections
 */
  
contract sequence over %t determines %e is {
  _empty has type ()<=%t;
  _pair has type (%e,%t)<=%t;
  _cons has type (%e,%t)=>%t;
  _apnd has type (%t,%e)=>%t;
  _back has type (%t,%e)<=%t;
  _nil has type ()=>%t;
}
  
contract concatenate over %t is {
  _concat has type (%t,%t)=>%t;
}
        
contract indexable over s determines (k,v) is {
  _index has type (s,k)=>v;
  _set_indexed has type (s,k,v)=>s;
  _delete_indexed has type (s,k)=>s;
  _index_member has type (v)<=(s,k);
}
  
contract sliceable over %t is {
  _slice has type (%t,integer,integer)=>%t;
  _tail has type (%t,integer)=>%t;
  _splice has type (%t,integer,integer,%t)=>%t;
}
  
-- The period gets in the way of the square brackets ... shuffle.
  
# #(?R)# . #(?F)# [?Ix] ==> _index(R.F,Ix); 
# #(?M)#[?Ix: ?Cx] ==> _slice(M,Ix,Cx);
# #(?M)#[?Ix:] ==> _tail(M,Ix);
# #(?M)#[?Ix: ?Cx] := ?Exp ==> M := _splice(M,Ix,Cx,Exp);
# _slice(?M,?Ix,?Tx) := ?Exp ==> M := _splice(M,Ix,Tx,Exp);
  
# #(?M)#[?Ix] := ?Exp ==> M := _set_indexed(M,Ix,Exp);
# _index(?M,?Ix) := ?Exp ==> M := _set_indexed(M,Ix,Exp);

# remove #(?M)#[?Ix] ==> M := _delete_indexed(M,Ix);
# remove _index(?M,?Ix) ==> M := _delete_indexed(M,Ix);
# #(?M)#[?Ix] ==> _index(M,Ix);
  
# prefix((present),500);
# present #(?M)#[?Ix] :: expression :- M::expression :& Ix::expression;
# present #(?M)# . #(?F)# [?Ix] ==> (M.F,Ix) matches _index_member(_);
# present #(?M)#[?Ix] ==> (M,Ix) matches _index_member(_);

# #(?M)#[?K] matches ?V ==> (M,K) matches _index_member(V);
# _index(?M,?K) matches ?V ==> (M,K) matches _index_member(V);
  
contract sorting over %c determines %t is {
  sort has type (%c,(%t,%t)=>boolean)=>%c
}
  
contract reversible over %t determines %e is {
  reverse has type (%t)=>%t;
}
  
#right((union),700);
#right((intersect),600);
#right((complement),500);
  
contract sets over %t is {
  (union) has type (%t,%t)=>%t;
  (intersect) has type (%t,%t)=>%t;
  (complement) has type (%t,%t)=>%t;
}

contract explosion over t determines e is {
  explode has type (t)=>list of e;
  implode has type (list of e) => t;
}